CHOICE-STRATEGY-IS: 
ANCESTRY∧SUPPORT[THEOREM]∧EQUALITY[=,3];

EDIT-STRATEGY-IS: 
DEMOD[4,3,2,1;4]∧(DEPTH[3]∨LENGTH[1]);

ELAPSED-TIME =3767

NIL 1 2
1 (x ⊗(y ⊗ z))=(z ⊗(y ⊗ x));G3
2 ¬((THEOREM3 ⊗ THEOREM2)⊗(THEOREM4 ⊗ THEOREM2))=(THEOREM3 ⊗ THEOREM4);THEOREM